(benchmark icbrtorinvalidvc.smt
:source {
Integer cube root algorithm icbrt(x), where x is an unsigned 32 bit integer.
From the book "Hacker's delight" by Henry S. Warren, Jr., page 212
We use "or" instead of "add" to increment values inside the loop.

We try to show the invalid verification condition:
y^3 == x or (y^3 < x and (y+1)^3 > x) holds, where y is the result.

Contributed by Robert Brummayer (robert.brummayer@gmail.com)
}
:status sat
:category { crafted }
:logic QF_BV
:extrafuns ((x BitVec[32]))
:formula
(let (?e2 bv30[5])
(let (?e3 bv0[32])
(let (?e4 bv1[32])
(let (?e5 bv2[32])
(let (?e6 bv3[32])
(let (?e7 bv3[5])
(let (?e8 (bvmul ?e3 ?e5))
(let (?e9 (bvor ?e8 ?e4))
(let (?e10 (bvmul ?e8 ?e6))
(let (?e11 (bvmul ?e10 ?e9))
(let (?e12 (bvor ?e11 ?e4))
(let (?e13 (bvshl ?e12 (zero_extend[27] ?e2)))
(let (?e14 (bvsub ?e2 ?e7))
(let (?e15 (ite (bvuge x ?e13) bv1[1] bv0[1]))
(let (?e16 (bvsub x ?e13))
(let (?e17 (ite (= bv1[1] ?e15) ?e16 x))
(let (?e18 (bvor ?e8 ?e4))
(let (?e19 (ite (= bv1[1] ?e15) ?e18 ?e8))
(let (?e20 (bvmul ?e19 ?e5))
(let (?e21 (bvor ?e20 ?e4))
(let (?e22 (bvmul ?e20 ?e6))
(let (?e23 (bvmul ?e22 ?e21))
(let (?e24 (bvor ?e23 ?e4))
(let (?e25 (bvshl ?e24 (zero_extend[27] ?e14)))
(let (?e26 (bvsub ?e14 ?e7))
(let (?e27 (ite (bvuge ?e17 ?e25) bv1[1] bv0[1]))
(let (?e28 (bvsub ?e17 ?e25))
(let (?e29 (ite (= bv1[1] ?e27) ?e28 ?e17))
(let (?e30 (bvor ?e20 ?e4))
(let (?e31 (ite (= bv1[1] ?e27) ?e30 ?e20))
(let (?e32 (bvmul ?e31 ?e5))
(let (?e33 (bvor ?e32 ?e4))
(let (?e34 (bvmul ?e32 ?e6))
(let (?e35 (bvmul ?e34 ?e33))
(let (?e36 (bvor ?e35 ?e4))
(let (?e37 (bvshl ?e36 (zero_extend[27] ?e26)))
(let (?e38 (bvsub ?e26 ?e7))
(let (?e39 (ite (bvuge ?e29 ?e37) bv1[1] bv0[1]))
(let (?e40 (bvsub ?e29 ?e37))
(let (?e41 (ite (= bv1[1] ?e39) ?e40 ?e29))
(let (?e42 (bvor ?e32 ?e4))
(let (?e43 (ite (= bv1[1] ?e39) ?e42 ?e32))
(let (?e44 (bvmul ?e43 ?e5))
(let (?e45 (bvor ?e44 ?e4))
(let (?e46 (bvmul ?e44 ?e6))
(let (?e47 (bvmul ?e46 ?e45))
(let (?e48 (bvor ?e47 ?e4))
(let (?e49 (bvshl ?e48 (zero_extend[27] ?e38)))
(let (?e50 (bvsub ?e38 ?e7))
(let (?e51 (ite (bvuge ?e41 ?e49) bv1[1] bv0[1]))
(let (?e52 (bvsub ?e41 ?e49))
(let (?e53 (ite (= bv1[1] ?e51) ?e52 ?e41))
(let (?e54 (bvor ?e44 ?e4))
(let (?e55 (ite (= bv1[1] ?e51) ?e54 ?e44))
(let (?e56 (bvmul ?e55 ?e5))
(let (?e57 (bvor ?e56 ?e4))
(let (?e58 (bvmul ?e56 ?e6))
(let (?e59 (bvmul ?e58 ?e57))
(let (?e60 (bvor ?e59 ?e4))
(let (?e61 (bvshl ?e60 (zero_extend[27] ?e50)))
(let (?e62 (bvsub ?e50 ?e7))
(let (?e63 (ite (bvuge ?e53 ?e61) bv1[1] bv0[1]))
(let (?e64 (bvsub ?e53 ?e61))
(let (?e65 (ite (= bv1[1] ?e63) ?e64 ?e53))
(let (?e66 (bvor ?e56 ?e4))
(let (?e67 (ite (= bv1[1] ?e63) ?e66 ?e56))
(let (?e68 (bvmul ?e67 ?e5))
(let (?e69 (bvor ?e68 ?e4))
(let (?e70 (bvmul ?e68 ?e6))
(let (?e71 (bvmul ?e70 ?e69))
(let (?e72 (bvor ?e71 ?e4))
(let (?e73 (bvshl ?e72 (zero_extend[27] ?e62)))
(let (?e74 (bvsub ?e62 ?e7))
(let (?e75 (ite (bvuge ?e65 ?e73) bv1[1] bv0[1]))
(let (?e76 (bvsub ?e65 ?e73))
(let (?e77 (ite (= bv1[1] ?e75) ?e76 ?e65))
(let (?e78 (bvor ?e68 ?e4))
(let (?e79 (ite (= bv1[1] ?e75) ?e78 ?e68))
(let (?e80 (bvmul ?e79 ?e5))
(let (?e81 (bvor ?e80 ?e4))
(let (?e82 (bvmul ?e80 ?e6))
(let (?e83 (bvmul ?e82 ?e81))
(let (?e84 (bvor ?e83 ?e4))
(let (?e85 (bvshl ?e84 (zero_extend[27] ?e74)))
(let (?e86 (bvsub ?e74 ?e7))
(let (?e87 (ite (bvuge ?e77 ?e85) bv1[1] bv0[1]))
(let (?e88 (bvsub ?e77 ?e85))
(let (?e89 (ite (= bv1[1] ?e87) ?e88 ?e77))
(let (?e90 (bvor ?e80 ?e4))
(let (?e91 (ite (= bv1[1] ?e87) ?e90 ?e80))
(let (?e92 (bvmul ?e91 ?e5))
(let (?e93 (bvor ?e92 ?e4))
(let (?e94 (bvmul ?e92 ?e6))
(let (?e95 (bvmul ?e94 ?e93))
(let (?e96 (bvor ?e95 ?e4))
(let (?e97 (bvshl ?e96 (zero_extend[27] ?e86)))
(let (?e98 (bvsub ?e86 ?e7))
(let (?e99 (ite (bvuge ?e89 ?e97) bv1[1] bv0[1]))
(let (?e100 (bvsub ?e89 ?e97))
(let (?e101 (ite (= bv1[1] ?e99) ?e100 ?e89))
(let (?e102 (bvor ?e92 ?e4))
(let (?e103 (ite (= bv1[1] ?e99) ?e102 ?e92))
(let (?e104 (bvmul ?e103 ?e5))
(let (?e105 (bvor ?e104 ?e4))
(let (?e106 (bvmul ?e104 ?e6))
(let (?e107 (bvmul ?e106 ?e105))
(let (?e108 (bvor ?e107 ?e4))
(let (?e109 (bvshl ?e108 (zero_extend[27] ?e98)))
(let (?e110 (bvsub ?e98 ?e7))
(let (?e111 (ite (bvuge ?e101 ?e109) bv1[1] bv0[1]))
(let (?e112 (bvsub ?e101 ?e109))
(let (?e113 (ite (= bv1[1] ?e111) ?e112 ?e101))
(let (?e114 (bvor ?e104 ?e4))
(let (?e115 (ite (= bv1[1] ?e111) ?e114 ?e104))
(let (?e116 (bvmul ?e115 ?e5))
(let (?e117 (bvor ?e116 ?e4))
(let (?e118 (bvmul ?e116 ?e6))
(let (?e119 (bvmul ?e118 ?e117))
(let (?e120 (bvor ?e119 ?e4))
(let (?e121 (bvshl ?e120 (zero_extend[27] ?e110)))
(let (?e122 (bvsub ?e110 ?e7))
(let (?e123 (ite (bvuge ?e113 ?e121) bv1[1] bv0[1]))
(let (?e124 (bvsub ?e113 ?e121))
(let (?e125 (ite (= bv1[1] ?e123) ?e124 ?e113))
(let (?e126 (bvor ?e116 ?e4))
(let (?e127 (ite (= bv1[1] ?e123) ?e126 ?e116))
(let (?e128 (bvmul ?e127 ?e5))
(let (?e129 (bvor ?e128 ?e4))
(let (?e130 (bvmul ?e128 ?e6))
(let (?e131 (bvmul ?e130 ?e129))
(let (?e132 (bvor ?e131 ?e4))
(let (?e133 (bvshl ?e132 (zero_extend[27] ?e122)))
(let (?e134 (bvsub ?e122 ?e7))
(let (?e135 (ite (bvuge ?e125 ?e133) bv1[1] bv0[1]))
(let (?e136 (bvsub ?e125 ?e133))
(let (?e137 (ite (= bv1[1] ?e135) ?e136 ?e125))
(let (?e138 (bvor ?e128 ?e4))
(let (?e139 (ite (= bv1[1] ?e135) ?e138 ?e128))
(let (?e140 (bvmul ?e139 ?e139))
(let (?e141 (bvmul ?e140 ?e139))
(let (?e142 (ite (= x ?e141) bv1[1] bv0[1]))
(let (?e143 (bvadd ?e139 bv1[32]))
(let (?e144 (bvmul ?e143 ?e143))
(let (?e145 (bvmul ?e144 ?e143))
(let (?e146 (ite (bvult ?e141 x) bv1[1] bv0[1]))
(let (?e147 (ite (bvugt ?e145 x) bv1[1] bv0[1]))
(let (?e148 (bvand ?e146 ?e147))
(let (?e149 (bvor ?e142 ?e148))
(not (= (bvnot ?e149) bv0[1]))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
